// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_LEX_DIGIT_H
#define _sHT_LEX_DIGIT_H

#include <stdint.h>

#ifdef __FRAMAC__
#  include <sHT/nospec.h>
#endif

/*@ axiomatic Digit {
      logic 𝔹 decimal_p(ℤ c) = '0' <= c <= '9';
      logic 𝔹 downaf_p(ℤ c) = 'a' <= c <= 'f';
      logic 𝔹 upaf_p(ℤ c) = 'A' <= c <= 'F';
      logic 𝔹 downhex_p(ℤ c) = decimal_p(c) || downaf_p(c);
      logic 𝔹 uphex_p(ℤ c) = decimal_p(c) || upaf_p(c);
      logic 𝔹 hex_p(ℤ c) = decimal_p(c) || downaf_p(c) || upaf_p(c);

      lemma dec_downhex: ∀ ℤ c; decimal_p(c) ==> downhex_p(c);
      lemma dec_uphex: ∀ ℤ c; decimal_p(c) ==> uphex_p(c);
      lemma dec_hex: ∀ ℤ c; decimal_p(c) ==> hex_p(c);

      lemma downhex_hex: ∀ ℤ c; downhex_p(c) ==> hex_p(c);
      lemma uphex_hex: ∀ ℤ c; uphex_p(c) ==> hex_p(c);

      logic ℤ digitval_undef;

      logic ℤ decimal_val(ℤ c) = decimal_p(c) ? c - '0' : digitval_undef;
      logic ℤ downaf_val(ℤ c) = downaf_p(c) ? c - 'a' + 10 : digitval_undef;
      logic ℤ upaf_val(ℤ c) = upaf_p(c) ? c - 'A' + 10 : digitval_undef;

      logic ℤ downhex_val(ℤ c) = decimal_p(c) ? decimal_val(c)
        : downaf_p(c) ? downaf_val(c) : digitval_undef;
      logic ℤ uphex_val(ℤ c) = decimal_p(c) ? decimal_val(c)
        : upaf_p(c) ? upaf_val(c) : digitval_undef;
      logic ℤ hex_val(ℤ c) = downhex_p(c) ? downhex_val(c)
        : uphex_p(c) ? uphex_val(c) : digitval_undef;
    } */

/* TODO which types are the most interesting?
   (Performance, ease of proving (no implicit casts),
   consistency) */
#define sHT_digit_val_t unsigned
#define sHT_digit_char_t unsigned

/* TODO: are return types other than uint8_t performance-wise interesting?
   In any case, unsigned is useful for SMT solvers are being confused
   by the implicit casts. */

/*@ requires c: NS ==> decimal_p(c);
    requires range: 0 <= c < 256;
    terminates \true;
    assigns \result \from c;
    ensures result: NS ==> \result == decimal_val(c);
    ensures range: NS ==> 0 <= \result < 10; */
static sHT_digit_val_t
sHT_decimal_val(sHT_digit_char_t c)
{
	return c - 0x30u;
}

/*@ requires c: NS ==> uphex_p(c);
    requires range: 0 <= c < 256;
    terminates \true;
    assigns \result \from c;
    ensures result: NS ==> \result == uphex_val(c);
    ensures range: NS ==> 0 <= \result < 16; */
static sHT_digit_val_t
sHT_uphex_val(sHT_digit_char_t c)
{
	c -= 0x30u;
	/* On speculative architectures, this is expected
	   to be compiled into a conditional select or increase. */
	if (c >= 10u)
		c -= (0x41u - 0x30u) - 10u;
	return c;
}

/*@ requires c: NS ==> downhex_p(c);
    requires range: 0 <= c < 256;
    terminates \true;
    assigns \result \from c;
    ensures result: NS ==> \result == downhex_val(c);
    ensures range: NS ==> 0 <= \result < 16; */
static sHT_digit_val_t
sHT_downhex_val(sHT_digit_char_t c)
{
	c -= 0x30u;
	/* On speculative architectures, this is expected
	   to be compiled into a conditional select or increase. */
	if (c >= 10u)
		/* c - '0' - (('a' - '0') - 10) = c -= 'a' + 10 */
		c -= (0x61u - 0x30u) - 10u;
	return c;
}

#endif
